G12 statement check: census of every Lean declaration in Math- (3,782 targets) and the reader repairs it forced - #752

A census of every Lean declaration in Math- by the G12 statement check, and the reader repairs the corpus forced. Unit CBZ0-G12-CENSUS-01N-20261104. Anthropic Claude, Claude Code session session_01NMeKEismAyeqgdB4sy2NJU (Claude01N). Own paths only (tools/cbz/statement_fuzz.py, tests/test_cbz_statement_fuzz.py, cbz/evidence/g12-statement-fuzz-01n/); no canonical surface. Credit 0. Scientific effect NONE.

Why now. The owner's addendum rule — no closure marked CLOSED without the empirical layer — is being applied to an index that Claude 54's accounting has routed group by group (CLOSED candidates, quarantines pending kernel replay). The layer had been run on two manifests only (main formal/, Math- formal/). This PR runs it on every theorem in Math- (16 Lean groups, 3,782 declarations at dfa9b30a, raw evidence snapshots excluded) so the index can carry, per declaration, either an applicable verdict or an explicit not applicable with the construct named.

Census mode. --lean-dir <dir> [--exclude <substring>]…: every theorem/lemma under a directory is a target with no manifest; byte-identical files are evaluated once (recorded as copies); definitions and carrier types are shared across the group; UNSUPPORTED reasons are classified into a histogram. Coverage evidence, never a gate (exit 1 unless everything is PASS).

Result (CENSUS.md): 7 PASS · 128 CORROBORATED · 0 FAIL · 3,647 UNSUPPORTED. Reachable content turned up where no manifest pointed: 33 real-arithmetic lemmas in the Math-#514 Gaussian package, 18 in the #536 determinant package, 7 in W3Scratch, 5 real-arithmetic lemmas inside the cap-packet topology (sp_curved_side_constants, l12_constants, l9_arith, two toy evaluations), 7 in the specification proofs, 5 in the D2 companions. The two CLOSED-track Gaussian-field packages (source_smooth_realization, source_lifetime_realization) have no reachable declaration: every statement quantifies over SmoothSample/RealizedData-style structures. Zero FAIL across the 135 decided statements, kernel-proved groups included, is the reader-soundness check. Two corroborations are marked WEAK (fewer than a quarter of the requested instances satisfied their hypotheses; c ^ 2 + s ^ 2 = 1 is hit at four points).

Reader defects the census exposed — fixed, with regression tests, before the receipts were taken. The first run corroborated Measurable (sourceA L) (with sourceA : ℝ → ℝ → ℝ) and passed Integrable (fun z => |z| ^ 8) (gaussianReal 0 1): structural predicates whose arguments the finite model does not carry were taken as true. Now (i) a conclusion that is only a structural predicate is UNSUPPORTED for every statement, not only when a model binder is present; (ii) a structural predicate holds only for a table, a subset, a lambda on the carrier or a model measure — a function on ℝ, an unknown measure or a structure makes it UNSUPPORTED; (iii) a function-valued definition (def f (L : ℝ) : ℝ → ℝ := fun x => …) is applied to its extra arguments or reported as a value the interpreter does not carry. 42 verdicts of the first run were withdrawn to UNSUPPORTED by these repairs. Also forced by the corpus: attribute-prefixed declarations on one line (@[simp] theorem …, previously missed), Unicode subscript identifiers (x₀ had been read as a numeral), nested projections (p.2.1), multi-token ascription types ((Set.univ : Set Ω)), and a parser exception now fails one declaration instead of its module. Tests 78 → 81 (→ 85 with the review repairs below), both modes -W error clean; the 58 adversarial probes of #742 still match; main formal/ 59/59 PASS and Math- formal/ 3 · 56 · 4 unchanged.

Review repairs (95e5de31; Codex 4471516437 · 4471516451 · 4471516464, each reproduced, then fixed, each with a regression test). (1) A returned function (def f : ℕ → ℝ := fun n => …) bound its parameters at the codomain type (n - 1 real where Lean truncates): parameters now take the domain types of the declared arrow (explicit binder types win), arrow types split at bracket depth 0 only. (2) Definitions pooled by short name, first module wins: now kept by Lean-qualified name with namespace/section/end/open tracked as scopes, resolved from the statement's namespace outward and through its opens, own module first, then the group only when exactly one definition (up to identical text) carries the name — otherwise UNSUPPORTED "ambiguous definition". (3) Declaration keywords recognised at column 0 only: indented declarations and open … in / set_option … in prefixes now start declarations, and a theorem/lemma keyword the splitter still cannot separate is an UNSUPPORTED target "declaration not reached by the parser" — every declaration in a file is accounted for. Exposure of the landed receipts was measured first: none (11 cross-module name collisions in the corpus, none referenced by a decided statement; no decided statement applied a returned function; no unreached declaration). Re-run with the repaired tool: 0 of 3,782 census verdicts and 0 package verdicts changed; 695 census targets now carry their Lean-qualified names (CapHyp.* → CapFirstExit.CapHyp.*); 14 UNSUPPORTED reasons are more specific; receipts re-taken (*_r4 package receipts equal r3 per target; 12 of 16 census receipts byte-identical).

6 November declaration-scope repair (Codex 4472023769; commit 55571918). A cross-namespace call selected the right definition but evaluated its body, pattern clauses and closures in the theorem/caller namespace, allowing both false FAIL and false PASS. Definitions and closures now retain their declaration namespace and open set, with caller scope restored in finally. A RED→GREEN regression covers ordinary bodies, returned functions, pattern clauses and open … in def with positive and false assertions. tests.test_cbz_statement_fuzz: 86/86 PASS in normal, -O, and -W error modes. Native re-run of all 16 Math- census groups at exact dfa9b30a: all 3,782 semantic JSON results unchanged after normalising only the environment-specific lean_dir field (7 PASS · 128 CORROBORATED · 0 FAIL · 3,647 UNSUPPORTED). Additive receipt: declaration_scope_repair_20261106.json; historical receipts unchanged. Full local discovery: 2,005 tests, 25 skips, one CPython-3.12 failure in test_outer_empty_guard_mutation_is_rejected, reproduced identically from detached unmodified 95e5de31 and not concealed.

Per-record annotation of the #695 index (g12_annotations_literal_index_82d9e480.json):''`` each of the 367 CLOSED records of cbz/evidence/kernel/all-closed-declarations.json (main#695 at `82d9e480`) is bound by (sha256 of its source file, qualified declaration name) to a census or package target — all 367 bind: 34 PASS · 69 CORROBORATED · 264 not applicable · 0 FAIL (main `formal/UniversalLaw` 31 PASS; Math- `ResearchFormalCoreR1` 3 · 56 · 4; determinant 13 CORROBORATED · 53 n/a; smooth 116, spec 78, c297 13 all n/a, construct named). Row text for Root: `G12: PASS | CORROBORATED | not applicable ()`. An annotation, not a CLOSED decision.

For the index (proposal, for Root; the parent README's B-007 text is amended accordingly). A CLOSED row carries G12: PASS | CORROBORATED | not applicable (<construct>) from the registered run or the census at its source cut; not applicable names the construct the interpreter does not model and is never written for a statement the interpreter reaches; UNSUPPORTED is never upgraded or left silent. The addendum rule is satisfiable only through that explicit path — and for the Gaussian-field packages it will read not applicable throughout, which the index should say rather than let the rule be read as satisfied. The next extension with measurable payoff is a finite-vector backend (Fin n → ℝ, Fin d → ℤ, ∑): several hundred binders. Statements over the field structures are beyond sampling.

Reproduce. git -C <Math- clone> archive dfa9b30a… frontiers companions specifications reviews formal | tar -x -C /tmp/g12-census/math, then bash cbz/evidence/g12-statement-fuzz-01n/census_math_dfa9b30a_20261104/run_census.sh from a main checkout (about 12 s, deterministic, seed 1 / 64 samples). SHA256SUMS binds the 16 receipts and 16 stdout summaries; file_sha256 in each receipt binds every Lean file read.

Integration. Base main (d2b0216e); current head ce1724f5 (four commits: original census/repairs 54bce0dd, review repairs 95e5de31, declaration-scope repair 55571918, additive qualification ce1724f5). Own paths only; no canonical surface. Review finding 4472023769 is repaired; its thread and the three earlier addressed review threads are resolved after exact-head hosted qualification. Current local validation: 86/86 statement-fuzz tests pass in normal, -O, and -W error; all 16 exact-source census reports are semantically unchanged. Full local discovery at the repaired bytes ran 2,005 tests with 25 explicit skips and one pre-existing interpreter-sensitive mutation-harness failure, reproduced from the unmodified 95e5de31 base. Hosted qualification for exact head ce1724f5 is complete: runs 42160061830, 42160061942, 42160061839, 42160061894, and 42160061810 all concluded SUCCESS; every one of their 10 jobs concluded SUCCESS. No default ref, foreign branch, theorem, bound, proof outcome, or historical receipt was changed. Next action: Root B-003 may perform the fresh-base serial integration under the required checks; no self-merge and no default-ref write occurred here.

Author's note (Claude01N, 6 Nov 04:35Z), after reading the repair delta 95e5de31..ce1724f5: the declaration-scope repair is sound and complete — every definition-body evaluation path (Var, apply direct / clauses / returned function / Measure recursion, _closure, materialize, at_point, call_values) now runs inside declaration_scope(d.namespace, d.opens) with the caller restored in finally; argument evaluation stays in the caller's scope, as it must. Reproduced at ce1724f5: 86/86 in normal and -O -W error; both package receipts (main_formal_ec6962ff_r4.json, math_formal_19a55750_r4.json) regenerate byte-identically. No author objection; the repair is the successor lane's work and stays as pushed. Checks at ce1724f5 so far: public-intake, public-shop, formal / formal-evidence, g11-auditor, drift-crawler-self-test, browser-smoke and federation-drift success (the main-side drift was repaired by #751/#754 on 5 Nov), navigation/architecture running, verify pending. The branch reads behind (main is at 62611e73): the base refresh is the integrating lane's, with a merge commit under an expected-old-ref guard. The REVIEW-752-ENG pickup by GROK-H03-ben at 95e5de31 (738/6646970260, 45-min lease) posted no RESULT and has lapsed; a nonauthor read of the two repair deltas at ce1724f5 is welcome, or the integrator's own read. The four answered Codex threads need resolving by the integrator (branch rule).

Authoritative hosted qualification update (6 November 2026). Exact head ce1724f505bfa6ee1235e8809bb54522862bf962, tree 22de186eb7a81ad11c7e227a3db8b913f845c82f: all five associated workflows and all ten jobs completed SUCCESS — G11 auditor 42160061830; federation drift 42160061942; public-shop 42160061839; research navigation/public source 42160061894; workspace-landing 42160061810 (formal, architecture, landing-checks, verify). The four answered review threads are resolved only after those conclusions were observed. This is PR qualification, not CBZ-0 or whole-federation qualification; the one local full-discovery failure remains truthfully bounded as the CPython-3.12 warning-to-oracle mutation-harness failure reproduced from unmodified 95e5de31. No default ref was changed.

Generated by Claude Code